0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 80 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 71 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇔, 0 ms)
↳16 QDP
↳17 MRRProof (⇔, 113 ms)
↳18 QDP
↳19 MRRProof (⇔, 26 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 TRUE
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U2_G(X1, X2, X3, leB_in_gg(X1, X2))
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → LEB_IN_GG(X1, X2)
LEB_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, leB_in_gg(X1, X2))
LEB_IN_GG(s(X1), s(X2)) → LEB_IN_GG(X1, X2)
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U3_G(X1, X2, X3, lecB_in_gg(X1, X2))
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → U4_G(X1, X2, X3, orderedA_in_g(.(s(X2), X3)))
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → ORDEREDA_IN_G(.(s(X2), X3))
ORDEREDA_IN_G(.(0, .(s(0), X1))) → U5_G(X1, orderedA_in_g(.(s(0), X1)))
ORDEREDA_IN_G(.(0, .(s(0), X1))) → ORDEREDA_IN_G(.(s(0), X1))
ORDEREDA_IN_G(.(0, .(0, X1))) → U6_G(X1, orderedA_in_g(.(0, X1)))
ORDEREDA_IN_G(.(0, .(0, X1))) → ORDEREDA_IN_G(.(0, X1))
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
lecB_in_gg(0, s(0)) → lecB_out_gg(0, s(0))
lecB_in_gg(0, 0) → lecB_out_gg(0, 0)
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U2_G(X1, X2, X3, leB_in_gg(X1, X2))
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → LEB_IN_GG(X1, X2)
LEB_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, leB_in_gg(X1, X2))
LEB_IN_GG(s(X1), s(X2)) → LEB_IN_GG(X1, X2)
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U3_G(X1, X2, X3, lecB_in_gg(X1, X2))
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → U4_G(X1, X2, X3, orderedA_in_g(.(s(X2), X3)))
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → ORDEREDA_IN_G(.(s(X2), X3))
ORDEREDA_IN_G(.(0, .(s(0), X1))) → U5_G(X1, orderedA_in_g(.(s(0), X1)))
ORDEREDA_IN_G(.(0, .(s(0), X1))) → ORDEREDA_IN_G(.(s(0), X1))
ORDEREDA_IN_G(.(0, .(0, X1))) → U6_G(X1, orderedA_in_g(.(0, X1)))
ORDEREDA_IN_G(.(0, .(0, X1))) → ORDEREDA_IN_G(.(0, X1))
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
lecB_in_gg(0, s(0)) → lecB_out_gg(0, s(0))
lecB_in_gg(0, 0) → lecB_out_gg(0, 0)
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
LEB_IN_GG(s(X1), s(X2)) → LEB_IN_GG(X1, X2)
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
lecB_in_gg(0, s(0)) → lecB_out_gg(0, s(0))
lecB_in_gg(0, 0) → lecB_out_gg(0, 0)
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
LEB_IN_GG(s(X1), s(X2)) → LEB_IN_GG(X1, X2)
LEB_IN_GG(s(X1), s(X2)) → LEB_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U3_G(X1, X2, X3, lecB_in_gg(X1, X2))
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → ORDEREDA_IN_G(.(s(X2), X3))
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
lecB_in_gg(0, s(0)) → lecB_out_gg(0, s(0))
lecB_in_gg(0, 0) → lecB_out_gg(0, 0)
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U3_G(X1, X2, X3, lecB_in_gg(X1, X2))
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → ORDEREDA_IN_G(.(s(X2), X3))
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
lecB_in_gg(0, s(0)) → lecB_out_gg(0, s(0))
lecB_in_gg(0, 0) → lecB_out_gg(0, 0)
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
lecB_in_gg(x0, x1)
U12_gg(x0, x1, x2)
lecB_in_gg(0, s(0)) → lecB_out_gg(0, s(0))
lecB_in_gg(0, 0) → lecB_out_gg(0, 0)
POL(.(x1, x2)) = 1 + 2·x1 + 2·x2
POL(0) = 0
POL(ORDEREDA_IN_G(x1)) = x1
POL(U12_gg(x1, x2, x3)) = x1 + x2 + x3
POL(U3_G(x1, x2, x3, x4)) = 1 + x1 + 2·x2 + 2·x3 + 2·x4
POL(lecB_in_gg(x1, x2)) = 1 + x1 + x2
POL(lecB_out_gg(x1, x2)) = x1 + x2
POL(s(x1)) = 2·x1
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U3_G(X1, X2, X3, lecB_in_gg(X1, X2))
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → ORDEREDA_IN_G(.(s(X2), X3))
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
lecB_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U3_G(X1, X2, X3, lecB_out_gg(X1, X2)) → ORDEREDA_IN_G(.(s(X2), X3))
POL(.(x1, x2)) = x1 + x2
POL(ORDEREDA_IN_G(x1)) = 2·x1
POL(U12_gg(x1, x2, x3)) = x1 + 2·x2 + x3
POL(U3_G(x1, x2, x3, x4)) = 2·x1 + 2·x2 + 2·x3 + x4
POL(lecB_in_gg(x1, x2)) = 2·x1 + 2·x2
POL(lecB_out_gg(x1, x2)) = 2 + x1 + 2·x2
POL(s(x1)) = 2·x1
ORDEREDA_IN_G(.(s(X1), .(s(X2), X3))) → U3_G(X1, X2, X3, lecB_in_gg(X1, X2))
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
lecB_in_gg(x0, x1)
U12_gg(x0, x1, x2)
ORDEREDA_IN_G(.(0, .(0, X1))) → ORDEREDA_IN_G(.(0, X1))
lecB_in_gg(s(X1), s(X2)) → U12_gg(X1, X2, lecB_in_gg(X1, X2))
lecB_in_gg(0, s(0)) → lecB_out_gg(0, s(0))
lecB_in_gg(0, 0) → lecB_out_gg(0, 0)
U12_gg(X1, X2, lecB_out_gg(X1, X2)) → lecB_out_gg(s(X1), s(X2))
ORDEREDA_IN_G(.(0, .(0, X1))) → ORDEREDA_IN_G(.(0, X1))
ORDEREDA_IN_G(.(0, .(0, X1))) → ORDEREDA_IN_G(.(0, X1))
From the DPs we obtained the following set of size-change graphs: